Nuprl Lemma : fpf-compatible-join-cap 0,22

A:Type, eq:EqDecider(A), B:(AType), fg:a:A fp B(a), x:Az:B(x).
f || g  f  g(x)?z = g(x)?f(x)?z  B(x
latex


Definitionst  T, x:AB(x), b, A, x(s), b, , Prop, f(x), xt(x), Top, a:A fp B(a), x  dom(f), P  Q, P & Q, P  Q, Unit, if b t else f fi, f  g, P  Q, f(x)?z, f || g, EqDecider(T), False, {T}
Lemmasfpf-join-ap-sq, fpf-ap wf, fpf-compatible wf, fpf wf, deq wf, not functionality wrt iff, fpf-join-dom, fpf-join wf, top wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-dom wf, fpf-trivial-subtype-top, bool wf, bnot wf, not wf, assert wf

origin